#!/bin/bash
# usage: ./count_schema.sh

# 设置目录
SPEC_DIR="../dsn24"
LOG_DIR="../countlogs"
BYMC_DIR="/home/user/bymc/bymc"

# 检查日志目录是否存在，如果不存在则创建
if [ ! -d "$LOG_DIR" ]; then
    mkdir -p "$LOG_DIR"
    echo "Created log directory: $LOG_DIR"
fi

# Define the list of specifications to check
SPECS=("liveness-chor1-byz.ta" "liveness-chor2-byz.ta" "liveness-friedman-byz.ta" "liveness-king-byz.ta" "liveness-rabin-byz.ta"
       "safety-chor1-byz.ta"   "safety-chor2-byz.ta"   "safety-friedman-byz.ta"   "safety-king-byz.ta"   "safety-rabin-byz.ta"   "safety-mostefa-byz.ta")
MPIS=("liveness-mostefa-byz.ta" "liveness-dumbo-byz.ta"  "liveness-abraham-byz.ta"  "safety-dumbo-byz.ta"  "safety-abraham-byz.ta")
# Loop over each specification
for spec in "${MPIS[@]}"
do
    case "$spec" in
        "liveness-chor1-byz.ta")
            properties=("round_term" "phase1" "phase2")
            ;;
        "liveness-chor2-byz.ta")
            properties=("round_term" "cb0")
            ;;
        "liveness-friedman-byz.ta")
            properties=("round_term" "cb0")
            ;;
        "liveness-king-byz.ta")
            properties=("round_term" "phase1" "phase2")
            ;;
        "liveness-rabin-byz.ta")
            properties=("round_term" "cb0")
            ;;
        "liveness-mostefa-byz.ta")
            properties=("cb0" "cb2" "cb4" "secondphase0" "nonblocking")
            ;;
        "liveness-dumbo-byz.ta")
            properties=("cb0" "cb2" "cb4" "cb5" "unaminity0" "nonblocking")
            ;;
        "liveness-abraham-byz.ta")
            properties=("cb0" "cb2" "cb4" "unaminity0" "nonblocking")
            ;;
        "safety-chor1-byz.ta")
            properties=("round_term" "agree0" "valid0")
            ;;
        "safety-chor2-byz.ta")
            properties=("round_term" "agree0" "valid0")
            ;;
        "safety-friedman-byz.ta")
            properties=("round_term" "agree0" "valid0")
            ;;
        "safety-king-byz.ta")
            properties=("round_term" "agree0" "valid0")
            ;;
        "safety-rabin-byz.ta")
            properties=("agree0" "valid0")
            ;;
        "safety-mostefa-byz.ta")
            properties=("nonblocking" "agree0" "valid0")
            ;;
        "safety-dumbo-byz.ta")
            properties=("nonblocking" "agree0" "valid0")
            ;;
        "safety-abraham-byz.ta")
            properties=("nonblocking" "agree0" "valid0")
            ;;
        *)
            echo "Unknown specification: $spec"
            ;;
    esac

    # Loop over the properties for the current specification
    for prop in "${properties[@]}"
    do
        log_file="$LOG_DIR/count_schema_"$spec"_"$prop".log"
        COUNTCOMMAND="$BYMC_DIR/verify $SPEC_DIR/$spec $prop -O schema.tech=ltl -O schema.incremental=1 -O schema.compute-nschemas=1"
        echo "start counting schemas for $spec_$prop"
        # 使用 timeout 命令设置最大运行时间为 30 分钟，并检查输出是否包含指定字符串
        for ((i=1;i<2;i++)); do 
            timeout 30m $COUNTCOMMAND | tee "$log_file" 2>&1 | grep -q "linear extensions to enumerate" && break
        done
    done
done